Новая философская энциклопедия - доказательств теория
Связанные словари
Доказательств теория
Доказательств теория первоначально появилась в связи с программой Гильберта (см. Формализм), с задачей обоснования того, что каждый формальный вывод содержательно интерпретируемого (реального) утверждения дает содержательно правильный результат, включающий в случае необходимости и соответствующее построение.
Одним из шагов по направлению к данной цели казалось доказательство непротиворечивости формальных теорий. Это средство незаметно подменило собой цель, и поэтому первым громко прозвучавшим результатом теории доказательств была теорема Гёделя о неполноте и ее следствие — о недоказуемости непротиворечивости.
Важным позитивным результатом является теорема П. С. Новикова: утверждение о существовании результата алгоритмического построения, доказанное в классической арифметике, дает верное следствие, и в том числе (грубую) оценку числа необходимых шагов построения. Эта теорема стала основой целого класса результатов современной теории доказательств, обосновывающих совпадение классической истинности и конструктивной обоснованности для многих видов утверждений (в последнее время такие результаты все чаще доказываются методами моделей теории). Следующим шагом в развитии теории доказательств, надолго предопределившим ее магистральное направление, стала формулировка Г. Генценом исчисления секвенций и естественного вывода и доказательство им теоремы нормализации для классического и интуиционистского исчисления секвенций. Содержательно теорема нормализации означает возможность перестроить любой формальный вывод в нормализованный вывод без лемм. Было ясно, что понятие нормализованного вывода применимо и к естественному выводу, но точную формулировку дал только Д. Правиц (1965). Хотя формально определение Правица является сложным, содержательный смысл его вполне прозрачен. Логических правил для каждой связки обычно два: правило ее введения, показывающее, как доказывать утверждения данного вида, и правило удаления, показывающее, как их применять. Напр., для импликации в классической и во многих других логиках правила имеют вид: Допустим А
В, исходя из А А=
Вопрос-ответ:
Похожие слова
Самые популярные термины
1 | 2287 | |
2 | 1815 | |
3 | 1768 | |
4 | 1759 | |
5 | 1673 | |
6 | 1611 | |
7 | 1524 | |
8 | 1493 | |
9 | 1491 | |
10 | 1471 | |
11 | 1445 | |
12 | 1444 | |
13 | 1423 | |
14 | 1418 | |
15 | 1318 | |
16 | 1291 | |
17 | 1276 | |
18 | 1271 | |
19 | 1264 | |
20 | 1245 |